This week, work on conversion checking in LTT3 and progress towards unification. Conversion checking turns out to be pretty much the same as before, Unification is a bit trickier because unification problems can be suspended pending further information (like, other metavariables being unsolved means that we may need to postpone a unification problem until another one is solved) so we need to remember which local definitions were in scope. It's not that it's tricky, it just needs a bit more infrastructure (which we'll probably use everywhere). Also, to do these things, I've needed some more details in the context, which fortunately are no different than previous attempts at implementing the core, so can be reused.

Some other thoughts from the week... One thing Idris 2 takes a while to do (okay, not that long, but it's noticeable and annoying) is loading in libraries that have been compiled to a binary representation of the type checked terms, and all the dependencies. That is, keeping track of the database of definitions and the relationships between them. And another thing it does too much of is rechecking things that don't actually need rechecking.

The goal here is to have a really interactive system and part of this means not reloading everything every time a definition changes. So we need to be a bit cleverer than tracking dependencies between source files, and there are things we can learn from Query Based compiler architectures.

Hang on, did I say database? And relations? Hmm... anyway, there's some perfectly good tools that can already do what I think we need to do, so once the basic type system is working, my plan is to see if it makes sense to represent type checked collections of definitions in an SQLite database, so that we can quickly find out what needs rechecking any time a single definition changes and save doing unnecessary rechecking of things which aren't affected. Plenty of details to work out here, of course, but that's the basic idea.